Termination Proof Script
Consider the TRS R consisting of the rewrite rules
1:
div
(X,
e
)
→
i
(X)
2:
i
(
div
(X,Y))
→
div
(Y,X)
3:
div
(
div
(X,Y),Z)
→
div
(Y,
div
(
i
(X),Z))
There are 5 dependency pairs:
4:
DIV
(X,
e
)
→
I
(X)
5:
I
(
div
(X,Y))
→
DIV
(Y,X)
6:
DIV
(
div
(X,Y),Z)
→
DIV
(Y,
div
(
i
(X),Z))
7:
DIV
(
div
(X,Y),Z)
→
DIV
(
i
(X),Z)
8:
DIV
(
div
(X,Y),Z)
→
I
(X)
Consider the SCC {4-8}.
The constraints could not be solved.
Tyrolean Termination Tool
(0.03 seconds) --- May 3, 2006